module Reduction
where
import Char (isAlpha,isSpace)
import List ((\\), nub, sort)
import TITypes
import ParseExpression
import Combinators

type Name = String

showSeq :: (Show a) => [a] -> IO ()
showSeq = putStr . unlines . (map show) 

foldExp :: (Name -> a) -> (a -> a -> a) -> (Name -> a -> a) -> Expr -> a
foldExp id app lam = rec 
    where rec (Var x)      = id x
          rec (App e1 e2) = app (rec e1) (rec e2)
          rec (Abs x e)   = lam x (rec e)

occursFree :: Name -> Expr -> Bool
occursFree x = foldExp (x==) (||) (\y r->x/=y && r) 


ids :: Expr -> [Name]
ids = sort . nub . (foldExp (:[]) (++) (:))

fresh :: Expr -> Name
fresh e = head (strings \\ ("":ids e)) 
    where strings  = "":[a:as | as <- strings, a <- ['a'..'z']]

--subst :: Expr -> Expr -> Name -> Expr
--subst :: Expr -> Expr -> Name -> IO ()
subst m@(Var y) n x  = if x==y then n else m
subst (App e1 e2) n x = App (subst e1 n x) (subst e2 n x)
subst m@(Abs y e) n x 
    | x==y || not (occursFree x e) = m
    | not (occursFree y n)         = Abs y (subst e n x)
    | otherwise                    = Abs z (subst e' n x)
    where
      z  = fresh (App m n) 
      e' = subst e (Var z) y

beta :: Expr -> Expr -> Maybe Expr
--beta :: Expr -> IO ()
beta (Abs x e) e2 = Just (subst e e2 x)
beta _         _  = Nothing

